Lemma zero_plus_n_equal_n:
  forall n, O + n = n.
Proof.
  intros.
  simpl.
  reflexivity.
Qed.